The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

minsort(Cons(x, xs)) → appmin(x, xs, Cons(x, xs))
minsort(Nil) → Nil
appmin(min, Cons(x, xs), xs') → appmin[Ite][True][Ite](<(x, min), min, Cons(x, xs), xs')
appmin(min, Nil, xs) → Cons(min, minsort(remove(min, xs)))
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
remove(x', Cons(x, xs)) → remove[Ite](!EQ(x', x), x', Cons(x, xs))

The (relative) TRS S consists of the following rules:

!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
<(S(x), S(y)) → <(x, y)
<(0, S(y)) → True
<(x, 0) → False
remove[Ite](False, x', Cons(x, xs)) → Cons(x, remove(x', xs))
appmin[Ite][True][Ite](True, min, Cons(x, xs), xs') → appmin(x, xs, xs')
remove[Ite](True, x', Cons(x, xs)) → xs
appmin[Ite][True][Ite](False, min, Cons(x, xs), xs') → appmin(min, xs, xs')

Rewrite Strategy: INNERMOST

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
appmin(0, Cons(x, xs), xs') →⁺ appmin(0, xs, xs')
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [xs / Cons(x, xs)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)